テクニカルレポート | GRACEセンター

(1)

GRACE TECHNICAL REPORTS

Proceedings of the First International Workshop on

Formal Methods Education and Training

Jim Davies, Jeremy Gibbons, Mike Hinchey and Kenji

Taguchi (editors)

GRACE-TR 2008–03 2008 October 28

CENTER FOR GLOBAL RESEARCH IN

ADVANCED SOFTWARE SCIENCE AND ENGINEERING NATIONAL INSTITUTE OF INFORMATICS

(2)

(3)

Foreword

Formal methods have an important role to play in the development of com-plex computing systems — a role acknowledged in industrial standards such as IEC 61508 and ISO/IEC 15408, and in the increasing use of precise modeling notations, semantic markup languages, and model-driven techniques.

There is a growing need for software engineers who can work effectively with simple, mathematical abstractions, and with practical notions of inference and proof. However, there is little clear guidance — for educators, for managers, or for the engineers themselves — as to what might comprise a basic educa-tion in formal methods. The present IEEE/ACM Software Engineering Body of Knowledge (SWEBOK), in particular, lacks the kind of specific information that teachers and practitioners need to establish an adequate, balanced programme of learning in formal methods.

The workshop onFormal Methods Education and Trainingprovided a fo-rum for the discussion of the key issues in formal methods education, with a particular focus upon the development and advocacy of a Formal Methods Body of Knowledge (FMBOK), analogous to the Institute of Project Management’s PMBOK. This BOK would facilitate the design of appropriate programmes of education and training — undergraduate, graduate, and professional — for mod-ern software engineers, as well as promoting the sharing of teaching approaches, educational tools, and teaching materials.

Contributions were invited on this theme, and on a number of related aspects of education and training in formal methods: teaching experience, both academ-ically and industrially; curriculum issues, and the relationship with computer science and software engineering; teaching methodologies; and the use of tools. The extended abstracts that were submitted were reviewed for relevance. A mixture of these extended abstracts and longer draft papers was presented at the workshop on 28th October 2008, co-located with theInternational Conference on Formal Engineering Methods at the Kitakyushu International Conference Center, Kitakyushu, Japan. This National Institute of Informatics technical re-port represents the workshop proceedings. After the workshop, full papers will be solicited for submission and rigorously peer-reviewed for a special journal issue to be published by ACM.

The Programme Chairs would like to thank the authors for their contribu-tions to the workshop, the Programme Committee for their efforts in reviewing, and the organizers of ICFEM for handling all the logistical arrangements.

(4)

Jeremy Gibbons Mike Hinchey Kenji Taguchi

(5)

Organizers

Programme Chairs

Jim Davies

University of Oxford, UK Jeremy Gibbons

University of Oxford, UK Mike Hinchey

Lero, University of Limerick, Ireland Kenji Taguchi

National Institute of Informatics, Japan

Programme Committee Members

Toshiaki Aoki

Japan Advanced Institute of Science and Technology, Japan Cyrille Artho

Advanced Industrial Science and Technology (AIST)/RCIS, Japan Raymond Boute

Ghent University, Belgium David Duce

Oxford Brookes University, UK Lars-Henrik Eriksson

Uppsala University, Sweden Chris George

UNU/IIST, China J. Paul Gibson

Telecom SudParis, France Shaoying Liu

Hosei University, Japan Hideaki Nishihara

Advanced Industrial Science and Technology (AIST)/CVS, Japan Wolfgang Reif

University of Augsburg, Germany Steve Schneider

University of Surrey, UK Jing Sun

(6)

T. H. Tse

University of Hong Kong, China Burkhart Wolff

Universit´e de Paris 11, France Wang Yi

Uppsala University, Sweden

External Reviewers

Holger Grandy

(7)

FORMAL METHODS versus ENGINEERING

Tom Maibaum

Department of Computing and Software McMaster University

1280 Main Street West, Hamilton ON, Canada [email protected]

(9)

Teaching Formal Methods in the Context of Software

Engineering

Shaoying Liu1

, Kazuhiro Takahashi2

, Toshinori Hayashi2

, Toshihiro Nakayama1,2

1

Hosei University

2 _{The Nippon Signal Co., Ltd., Japan}

Abstract. Formal methods were developed to provide systematic and rigorous techniques for software development, and they must be taught in the context of software engineering. In this paper, we discuss the importance of such a teaching paradigm and describe several specific techniques for teaching formal methods. These techniques have been tested over the last fifteen years in our formal meth-ods education programs for undergraduate and graduate students at universities as well as practitioners at companies. Our experience shows that students can gain confidence in formal methods only when they learn their clear benefits in the context of software engineering.

1 Introduction

Despite more than forty years of effort to develop various theories, languages, methods, and tool supports, practical software engineering is still like a “desert”, lacking directions and effective ways of finding the way out of the software crisis. Formal methods were developed to address this problem by providing mathematically-based techniques, including formal specification, refinement, and verification. In theory, we now know how to use formal notations to write specifications, use refinement calculus to gradually transform a specification into a correct implementation, and use Hoare or Dijkstra’s logics to prove pro-grams correct with the same degree of the rigor that we apply to mathematical theorems. However, none of these techniques is easy to use by ordinary prac-titioners to deal with real software projects. The problem is the complexity of formal methods and the difficulty in manipulating mathematical formulas.

(10)

engineering methods [1], not formal methods. For example, the SOFL formal engineering method provides a three-step approach to constructing formal spec-ifications to help requirements analysis and system design, and specification-based review and testing for detecting bugs in both specifications and programs [2]. Software projects are human activities; they must be completed by required time and within specified budget, and they often face the instability of develop-ment teams. In such a situation, completely applying formal methods is rarely practical, but the improvement of software quality can be realized by equipping the developers with a disciplined manner and rigorous way of thinking through formal methods education.

In order to encourage more software developers to learn formal methods, we must first build up their motivation by demonstrating the clear benefits of formal methods in improving current software engineering practice. In fact, this is rather challenging and even more difficult when more and more young people become less interested in mathematics, especially in Japan. Nevertheless, this seems the only way we can possibly move forward in formal methods educa-tion. In this paper, we describe several techniques for teaching students formal methods. The fundamental idea is to put the formal methods education in the context of software engineering as far as we are concerned. Of course, as Parnas pointed out [3], formal methods should not be restricted to software engineering, but linked to and integrated in general engineering mathematics.

2 Teaching Techniques

In this section, we introduce some specific techniques for teaching formal meth-ods. These techniques have been tested by the first author over the last fifteen years of teaching VDM [4], SOFL [1], and Morgan’s refinement calculus [5] at universities and companies.

2.1 Starting with Examples

(11)

2.2 Gradual Introduction to Important Concepts

The fundamental concepts are the key to understand the spirit of formal meth-ods. It is quite effective to help students understand the essential principle of formal methods if sufficient efforts are made to teach the concepts. For exam-ple, when introducing formal specifications, we focus on the illustration of pre-and post-conditions. An effective way to teach the pre-post concept is by com-paring them with the corresponding algorithm and let students understand the real difference and relation between a specification and an algorithm. The com-parison can be made on the basis of simple scientific computation. For example, we often use the operation for yielding the square root of an integer as an exam-ple. The pre-condition of the operation isx ≥ 0and the post-condition of the operation can bey2

=x, wherexis input andyis output. But the corresponding algorithm would be something likey=M ath.sqrt(x). This example gives rise to a problem that outputyproduced by the algorithm may not satisfies the post-condition of the operation because the algorithm obtains only an approximation of the real square root of some positive integers. In this circumstance, it is use-ful to tell the students the importance of noticing this inconsistency between the specification and the implementation. This is also a good example to show the need for using or building proper theories in the application domain.

Furthermore, an operation specified using pre- and post-conditions defines a way of transforming an initial state to a final state. In order to let students understand this essential idea, making great efforts on the explanation of the fundamental concepts, such as state, type, and variable declaration, is helpful. The explanation can be given from different angles, for example, from the views of both mathematics and software. After students understand the basic concepts, we can then show them, with simple examples, how an algorithm transforms an initial state to a final state step by step through its statements, and how such a transformation can be abstracted into a pre- and post-conditions. This way of teaching helps students build an association between programs and specifica-tions, which paves the way for teaching specification-based verification tech-niques, such as formal verification, review, testing, or their combinations late on.

2.3 Massive Exercises on Basics

(12)

program is to let students do exercises immediately after a data type is intro-duced. For example, after the introduction of the set types, students must learn the meaning of the operators, such as union, intersection, cardinality, member-ship, subset, proper subset, and so on by applying them to specific set values. If time allows, a public discussion on students’ results is helpful. According to our experience, such a discussion can help capable students find out the reason for their mistakes and ordinary students find out the correct way of thinking. This training is similar to the basic training in sports. To be an excellent foot-ball player, for example, one must run fast and have a strong body. To build up these qualities, he or she must spend much time and make great efforts in the basic training. Anybody who ignores the basic training will fail to perform satisfactorily in matches.

The same principle is applicable to the teaching and study of formal refine-ment and verification techniques. To master the refinerefine-ment calculus, students must be required to do many small exercises on applying every refinement law in the calculus. To be skillful for formal verification, students must be required to do the same in understanding the meaning of each axiom and inference rule in the corresponding logics and their applications to small programs. The im-portant point here is to let them understand the underlying principle and skills of these techniques so that they will be possibly apply them, even informally, in practice.

2.4 Teaching Specification Patterns for Abstraction Skills

(13)

integers is empty? To answer this question, we first define a collection of inte-gers as asetand asequencein SOFL (or VDM), respectively, such asint set:

set of intandint seq:seq of int. We then discuss the most commonly used specification patterns for each of the data abstractions. For example, for the set of integers, we can use the following patterns to express the fact that the set is empty: int set= {} andcard(int set) = 0. Of course, we could have more patterns to express the same meaning, but those would be much more complex and no good for readability. For instance, a possible pattern can be: f orall[x:

int]|x notin int set. It is up to the teacher to decide whether to discuss such a complicated pattern within the required teaching time. In the case of a se-quence of integers, we can use the following patterns to express the fact that the sequence is empty:int set= []andlen(int set) = 0.

After each basic specification pattern is mastered by students, we can then go further to explain how such basic patterns can be applied in a more compli-cated situation. Let us take an operation to search for an integer in a collection of integers as an example. To explain how such an operation is specified, we take the same approach as the one to teaching the basic patterns by first defining the collection of integers asa set of integersanda sequence of integers, respec-tively, and then explaining how the operation can be specified by combining the basic patterns for each of the data abstractions.

2.5 Practice through Small Projects

(14)

and process decompositions. In fact, many existing formal notations focus only on one aspect of the problem in software engineering and ignore the others, but a real software project needs to take care of all possible aspects. If a method or technique merely helps solve one problem but create more other problems in the context of software engineering, it is unlikely to be popular among practitioners and to be applied in real projects. In this regard, the SOFL method has shown to be the exception, because it provides a systematic and rigorous process to integrating formal techniques into existing software engineering practices and creates no more problems.

2.6 Teaching Formal Methods Using Formal Engineering Methods

The ultimate goal of teaching formal methods (FM) is to create possibility of students applying them in practice. Formal engineering methods (FEM) show how FM can be applied in real projects. One of the very important aspects of FEM is the emphasis of combining diagrams, formal notation, and natural lan-guage in a coherent and systematic manner for writing specifications [1]. The purpose of this is to help the developer easily understand the specifications they are writing and the specifications written by others. Visualization is intuitive and suitable for describing the overall idea and system architecture; formal notation has a strength to achieve preciseness of statements in specifications; and natural language can be used to provide a friendly interpretation of formal expressions. In general, FEM differs from FM in that FM tries to answer the question “what should we do and why?” in software development, but FEM tries to answer the question “what can we do and how?”. To this end, FEM focuses on techniques and methods for integrating formal methods into the entire process of software development so that the strength of formal methods can be utilized in practice and their weakness of being complex can be avoided. FEM offers how soft-ware systems, including all level documents, are actually created and expressed formally, not just a simple mixture of formal notations with pictures. Since a de-tailed introduction to FEM is beyond the scope of this paper, we refer the reader to the SOFL book [1] for a comprehensive description of FEM.

(15)

informal explanations in English, the meaning of the whole operation specifica-tion can be easily digested by students.

2.7 Tool Support in Education

Almost all of us may have experienced using tools in teaching programming languages, such as Java and C, and found that it is effective to help students write, execute, and test programs (they need many pre-defined packages). Many of formal methods educators apply this idea to the teaching of formal meth-ods courses as well. However, our experience in teaching both VDM and SOFL courses, which focus on formal specification techniques, suggest that using tools in teaching formal methods is not necessarily effective; perhaps less effective than not using tools in some circumstances. There are two reasons. One is that learning formal methods requires students to learn both syntax and semantics of the related specification language. The most effective way for students to re-member them is to write formal specifications by hand, as they learn English as a foreign language. It is feasible, because exercises assigned to students in classes are of small scale. It is also effective in strengthening students’ memory of the syntax and in deepening their understanding of the abstraction techniques, because students would have no chance to “copy and paste” without thinking by themselves, as we often do on a computer. Another reason is that the purpose of writing a specification is not for a computer to directly run it, but for peo-ple (including himself or herself) to read and to understand. Therefore, letting themselves write a good style of formal specifications by hand is much more helpful for learning than by using a tool to automatically improve the style and format of their specifications. In the case of programming, without a tool, such as a compiler, we cannot run the program. But in the case of writing a specifi-cation, there is no need to run it, so without a tool support will not create any significant inconvenience. Instead, for some students who do not want to study formal methods, tool support will create chances for them to “copy and paste” without thinking.

(16)

methods by hand. This is similar to the situation where a person feels happy when he or she has a chance to eat delicious food after a long time starving.

2.8 Dealing with Time Constraint

Mathematical concepts and expressions usually require students to take time to digest, the teaching of them should take slow pace with many examples. How-ever, a course is like a software project: it also has time constraint. As a teacher, we often face a dilemma. On the one hand, we want to teach more contents which are all important for studying formal methods, but on the other hand, we do not have enough time. To tackle this problem, our experience suggests that each course should not be too ambitious; instead, it should be focused. For ex-ample, we can teach formal specification, refinement, and formal verification in three different courses, and it would be effective to focus the teaching in each of them on the most fundamental but important parts and give students suffi-cient time for them to apply the learned techniques. For example, when teaching SOFL, particularly techniques for writing formal specifications using pre- and post-conditions, to students, we usually take the interleaving approach: teaching concepts and asking students to practice using them. After finishing the whole course, we ask students to carry out a small project in which all knowledge learned is required to use. Such a way provides students with many opportuni-ties to learn how theoretical results can be effectively applied in practice.

2.9 Continuing Education

(17)

attractive to students. Our experience has suggested that to be attractive, formal methods must achieve a good balance among the three qualities: simplicity, vi-sualization, and preciseness, and must also demonstrate its benefits in ensuring software quality and reducing the cost of software projects as well as providing fun for students, such as computer graphics or animation, but unfortunately, few of existing formal methods have satisfied these criteria and it is hard to imag-ine that any teaching method would significantly improve this situation. Since software development needs mathematical way of thinking, we believe that no matter whether formal methods are attractive or not, education in formal meth-ods must continue at university and hopefully in industry as well. Only formal methods education can make the application of formal methods, either directly or indirectly, in software engineering possible.

3 Conclusions

Education is the necessary and most effective way to transfer formal methods to software industry. The most important influence factor for the success of formal methods education is whether the education is put in the context of software engineering. In this paper, we have described several techniques for teaching formal methods in the context of software engineering to both experienced and inexperienced students, each of which has been tested in practice. We believe that no matter whether formal methods can be used as an effective software en-gineering technique in practice, their education will definitely benefit software engineering practice. The only way to effectively transfer formal methods to industry is: education, education, and education.

References

1. S. Liu,Formal Engineering for Industrial Software Development Using the SOFL Method, Springer-Verlag, ISBN 3-540-20602-7, 2004.

2. S. Liu, A. J. Offutt, C. Ho-Stuart, Y. Sun, and M. Ohba, SOFL: A Formal Engineer-ing Methodology for Industrial Applications, IEEE Transactions on Software Engineering, 24(1):337–344, January 1998. Special Issue on Formal Methods.

3. D. L. Parnas,Education for Computing Professionals, Computer, 23(1):17-22, 1990. 4. C. B. Jones,Systematic Software Development Using VDM, 2nd edition, Prentice Hall, 1990. 5. C. Morgan,Programming from Specifications, 2nd edition, Prentice-Hall, 1994.

(18)

Formal Methods: Teaching and Practicing

Computer Science at the University Level

Raymond Boute

INTEC — Ghent University, Belgium,

[email protected] http://www.funmath.be

Abstract. At too many universities, CS curricula are not taught at the university level. This causes stagnation in professional practices. The missing element is the pervasive presence of mathematical modeling throughout the curriculum. This is the role of formal methods (FM) in its original sense. Mathematical fundamen-tals and concepts are crucial, software tools are secondary and even misleading without the former.

Social, professional, educational and local influencing factors are discussed. Recommendations are given for for curriculum structure, for specific key cources and for attitudes to instill in students and educators. As a conclusion, FM should break outside the limitations caused by the conservatism of policy makers but also the self-imposed ones.

1 Observations

Conventions Drawing boundaries between Computer Science and Engineering is more in the interest of departmental power games than epistemologically use-ful, so we take CS in a wide sense, including (even adopting) the engineering view.

Parnas [21] observes that “Professional engineers can often be distinguished from other designers by the engineers’ ability to use mathematical models to de-scribe and analyze their products”. The central role of mathematics is a fortiori evident to those viewing CS as a more theroretical activity than engineering.

Hence the use of mathematical modeling is a proper working criterion for what constitutes “university level” in teaching as well as in professional practice.

For completeness, some earlier material [5] will be recalled in passing.

1.1 The level of Computer Science curricula

In classical pure science and engineering disciplines, the pervasive use of math-ematics throughout the curriculum has become self-evident since centuries.

(19)

Still, too many universities teach CS at the level of pre-Newtonian mechan-ics. When colleagues who teach classical engineering courses (say, electronics) look at the computing courses in such curricula, they often remark that these courses are merely descriptive, lacking in intellectual content, and altogether little more than inflated programming courses—an opinion reinforced by the kind of assignments: writing programs, more programs and reports, and doing uninstructive projects [20]. Unfortunately, this remark is all too often justified.

Indeed, many CS curricula seem to be designed as a refuge for mathpho-bic students just to increase the student count. The study by Tucker et al. [28] uses American data, yet reflects European trends equally well (see section 3.3). Instead of devoting the scarce teaching resources to solid fundamentals [20], they are wasted on trendy topics that students could easily pick up on their own. Courses like “Introductory Programming” usually teach some language (which is better learned in passing via the assignments) rather than program design.

Formal Methods, if taught at all, have a small place in the curriculum, look-ing like an afterthought. Students see this as the best “proof” of their uselesness: if FM were af any value, wouldn’t all professors use them? Very few students are mature enough to see that curricula reflect the faculty [12] rather than relevance.

1.2 The level of professional practice

It is eery to see how little software practice has changed over the past 50 years. Some younger software professionals suggest that things were better in the “old times” [24]. For instance, Spolsky also notes that “programmers seem to have stopped reading books” [25]. However, a 1975 paper [19] already com-mented on the computer illiteracy of professional programmers!

Google yields ample comments on the phrase “Programmers don’t read”, indicating that many programmers find the books worthless anyway. However, the titles quoted in the rejection are on programming languages, not program analysis or design. This just reflects the old misconception that the main capa-bility of a programmer is the language.

Lethbridge surveyed “what knowledge is important to a software profes-sional” [17]. The use of the preposition “to” rather than ”for”, also in the cited paper’s abstract, is significant: it indicates that the survey is about subjective views. Circumstantial evidence leaves little doubt that many topics score low with the “average programmer” because they are not sufficiently known or mas-tered to be applied, rather than because they are truly less relevant or useful.

(20)

may be wise to use this information to detect the gaps, and educating profes-sionals in what they need for advancing their professionalism rather than what they want, which is just more of the same in what they already know.

An important question is: how could the extreme conservatism that has been dominating software practices over the past 50 years survive, whereas practice in other engineering disciplines has kept abreast with technology? The answer is manifold, but the common element is complacency.

– Software thrives on the spectacular advances in hardware technology. In-creased circuit speed and density often compensate for the stagnation in software design practices.

– Every few years some “method” is promoted that relies on acronyms rather than intellectual content, yet promises panacea with little effort. By con-trast: formal methods promise considerably less and require more effort. In other words, adapting Gresham’s law somewhat, “continuous injection of bad commodities keeps the good ones out of circulation”.

– In the economic situation of the recent decades, computer and information technology have seen continued growth with only rare periods of faltering. Due to this fast pace, there always are plenty of urgent development tasks to be done at all levels. Even people with no computing background who in-vest a minor effort in self-study can contribute usefully, and many well-paid tasks are easily learned “on the job”. With the urgent demand for quantity, and industry still uncertain about the exact qualifications software designers need, level and scientific basis are easily neglected.

The main problem is that many universities cater for the latter category, and actually advertise this attitude as “being responsive to the demands of industry”. Demands maybe, needs certainly not. Students do deserve better.

Students are also the key. Indeed, Max Planck is reputed to have said

Eine neue wissenschaftliche Wahrheit pflegt sich nicht in der Weise durchzusetzen, daß ihre Gegner überzeugt werden und sich als belehrt erklären, sondern vielmehr dadurch, daß ihre Gegner allmählich aussterben und daßß die heranwachsende Generation von vornherein mit der Wahrheit vertraut geworden ist.

Translated: “A new scientific truth usually does not break through in such a manner that its opponents are convinced and declare themselves informed, but rather because its opponents gradually die out, and the emerging generation has become familiar with it beforehand.” The task of the universities is clear.

(21)

es-sentially remain limited to the industries who benefit and the participanting re-searchers.

The effective lever for FM is not convincing the practitioners but educating the emerging generations.

2 Realizing the full potential of Formal Methods

2.1 Formal Methods

As observed by Gopalakrishnan [10], the term “formal methods” seems to sug-gest the sudden discovery by computer scientists of the use of mathematics—so evident in other branches of engineering that a separate appellation is redundant. Still, the specific term could be justified by the fact that CS/ECE requires a more formal kind of mathematics than the classical mathematical/engineer-ing disciplines, a point also emphasized in Lamport’s book on specifymathematical/engineer-ing sys-tems [14].

Here “formal” means that expressions are manipulated on the basis of their form (syntax) following precise calculation rules. This contrasts with traditional practice in math/engineering, where expressions are often manipulated on the basis of their interpretation (semantics) in some application domain. The benre-fit is in letting the symbols do the work, which is especially useful in areas where intuition for the application domain is still nascent. It also develops a “parallel intuition” for handling symbols that supports domain-oriented intuition [7].

Understood in this wider (actually, more original) sense, Formal Methods point the way not only to teaching CS at the university level, but also provides a refreshing new style to mathematics [9]. The realization has been demonstrated for discrete mathematics [11] and essentially all of engineering mathematics [4, 6].

Hence the non-CS engineering mathematics can equally benefit, and the entire curriculum considerably streamlined by unification.

2.2 The role of tools

To realize the aforementioned potential of FM, the use of software tools has to be led into the proper channels.

(22)

In mathematics, classical engineering and CS/ECE, software tools are meant to alleviate the burden of handling tedious details in calculations and proofs, and to reduce mistakes or avoiding pitfalls. Yet, this works only for users with am-ple mathematical maturity: for novices it can only lead to sorcerer’s apprentice attitudes and even ruin [13]. Indeed, current tools are far from mature:

– No single tool has sufficient scope; even small systems require multiple tools;

– Implementation restrictions cause a very narrow view on mathematics; – The many irrelevant syntax details and even semantic errors confuse novices.

For instance, tools like Maple and Mathematica seem designed fairly well for calculus and algebra, but in nearly every use for discrete mathematics the au-thor found calculations going astray in unexpected and educationally hazardous ways. Here is an example, arising from number representation. Consider the functions

– digitssuch that, for any natural number n, the base 10 representation isdigits(n), defined as a function such thatdigits(n)(i)is thei -th digit; in Maple:digits := n -> i -> floor (n/10ˆi) mod 10;

– decnum such thatdecnum(f)(k)is the number represented by the k

lowest digits in representation (function)f;

in Maple:decnum := f -> k -> sum(f(i)*10ˆi, i = 0..k-1);.

One expects decnum(digits(n))(k) = n if k digits suffice to repre-sentn. Yetdecnum(digits(210))(3);yields 620 whiledecnum(i -> i)(3); yields 210. The idea that “tools help students discover their errors” thus gets a new meaning!

In mathematics education, the trap of thinking that tool use can obviate solid mathematical reasoning abilities seems to have been largely avoided. Some cal-culus textbooks [27] even wisely contain examples and assignments involving tool use especially to foster awareness of the pitfalls. Likewise, insofar as Rston [22] advocates tools over pencil-and-paper simulation of computational al-gorithms (e.g., “long division”) in elementary school, he does not do so at the cost of reduced awareness for numbers and mathematics. To the contrary: he proposes more emphasis on head calculation as an antidote to rote and the er-rors typical for using calculators without numeric awareness.

(23)

“students should have the appropriate mathematical preparation [such as] cal-culus and differential equations”.

Unfortunately, in the FM area tools are often advertised as “hiding the math” for professionals (thus depriving them of the most powerful intellectual tool) and depicted by some lecturers as an aid to learn math for students (instead of mathematics preparing for tools). Tools are popular because they cater for the affinity of some students for video games, while seemingly “realistic” tool-based projects give them the illusion of becoming “real engineers” quickly and easily: the “sics munce ago i coodnt evun spel enguneer, now i are won” syn-drome.

Proper FM courses are essentially mathematical, do not teach tools, but con-tain assignments where students learn the use of tools and their defects.

3 Curriculum and course design

3.1 The mathematics content of engineering curricula

Learning by analogy from classical engineering disciplines and also consid-ering the huge body of mathematical knowledge generated by CS in recent decades [10], we propose the mathematical content for a computing engineering curriculum.

Table 1.Fundamental engineering mathematics at various levels

(level) EM. Engineering Math. CM. Computer Engineering Mathematics Basic Analysis, Linear algebra Formal proposition and predicate calculus (general) Probability and Statistics Function(al)s, relations, orderings

Discrete mathematics Lambda calculus (basics)

(combinatorics, graphs) Lattice theory, induction principles,. . . Targeted Physics, Circuit theory, Formal languages and automata (modeling) Control theory Formal language semantics

Stochastic processes Concurrency (parallel, mobile calculi etc.) Information Theory,. . . Type theory,. . .

“Advanced” Functional analysis Category theory Distribution Theory Unified algebra Hilbert and Banach spaces Modal logic

Measure theory,. . . Co-algebras and co-induction,. . .

(24)

“ba-sic” is domain-independent, “targeted” is more domain-oriented. We put “ad-vanced” in quotes because it is debatable: given today’s state of the art, some topics are arguably valuable for undergraduates as well.

EM is mathematics for classical engineering, e.g., electrical (EE). CM is the mathematics for Computing Engineering (CE). In view of curriculum design, the columns are meant to complement, not replace each other.

Indeed, considering just the first two rows, the EM topics are generally (and rightly) considered crucial in the formation of every engineer, and there is no reason to start making exceptions for CE’s, to the contrary [20]: CE’s can learn from the rich variety of examples and styles in mathematical modeling.

Conversely, the new mathematical style that emerged from Computing Sci-ence [9] is relevant to all exact sciSci-ences, as amply demonstrated for discrete mathematics [11] and for engineering mathematics in general [6]. For instance, [6] shows that it is useful for electrical and computer engineers (ECEs) to be as fluent in calculating with quantifiers (∀,∃) as with derivatives and integrals.

3.2 A Bachelor program in Computer Engineering

A program following the principles set out thus far is outlined in table 2. Note that it is a concept program, intended as an archetype for curriculum design by tailoring it to the local goals and possibilities. It can also be extended by either a 4th Bachelor year or a 2-year Master program.

Whereas most of the topic titles are familiar, the added value is in the unified mathematical modeling throughout all courses. In other words, the use of For-mal Methods is ubiquitous, obviating a separate course named “ForFor-mal Meth-ods”.

The basis is a first-semester course in logic in a form that is useful in the spirit of Gries [12], not only for CS but for all of engineering mathematics, starting with analysis. To reflect this, we called it Application-Oriented Formal Logic. The style is calculational. We briefly outline one actual realization. Apart from the usual proposition calculus (e.g., [11]), the two main elements provided are

a. Generic functionals [4]: using higher order functions supporting systems modeling and mathematical reasoning in a point-free style, and smooth con-version between point-free and the more common pointwise style.

b. Functional predicate calculus [6], supporting the aforementioned fluency in calculating with quantifiers in the context of applications.

(25)

Table 2.A concept BCE Program (3 years, extensible to 4)

First semester Second semester

6 Application-Oriented Formal Logic 6 Physics B (electricity & magnetism) 6 Mathematical Analysis A 6 Mathematical Analysis B

3 Algebra 3 Languages and Automata

3 Geometry 3 Disctete Math (combinatorics, graphs)

6 Physics A (particle & wave mechan.) 6 Classical Mechanics

6 Introductory Programming 6 Algorithms and Data Structures

Third semester Fourth semester

6 Probability and Statistics 6 Programming Languages

6 Complexity 6 Thermodynamics, heat & mass transfer

6 Signals and Systems 6 Database & Information Systems 3 Elements of Quantum Mechanics 3 Elements of Quantum Computing

3 Basic Electronics 3 Electrical Networks

6 Computer Architecture 6 Operating Systems

Fifth semester Sixth semester

6 Chemistry 3 Properties of Materials

3 Digital Systems 3 Elements of Relativity

3 Information Theory 6 Communications Systems

6 Concurrency 6 Communication Networks & Protocols

6 Software Engineering A 6 Software Engineering B

6 Embedded Systems 6 Hybrid Systems

(Legend: the numbers are a measure for the size of the course — see text)

and tools in the various other courses. No valuable time is wasted on “teach-ing” tool use or language features: these are picked up via the assignments. The courses themselves are fundamental and the appropriate body of knowledge can be structured around mathematical modeling (analysis, specification, design).

This point characterizes the curriculum, rather than a detailed listing of the topics in each course, which would be beyond the scope of a paper anyway. Yet, some additional observations help convey the guiding idea of “unity in diversity”.

Many non-CS courses are included, such as physics and engineering, for two reasons: (a) to enhance professionalism, as many students will need some clas-sical engineering in their later career [20], (b) to broaden the intellectual horizon and bring students in contact with a wide variety of modeling techniques.

(26)

For instance, arguably the best language choice for Introductory Program-ming is Scheme, with Abelson and Sussman [1] as a reference textbook. Of course, programming assignments should use Haskell as well. This background in computing meets with Physics A in Classical Mechanics (Sussman and Wis-dom [26]). The Lagrange-Hamilton approach used to be covered in classical engineering curricula and has been neglected for some years (perhaps for being less intuitive initially), but the time is ripe for reinstating it. This also paves the way for the later courses on quantum mechanics and quantum computing.

Algorithms and Data Structures emphasizes formal specification and deriva-tion of algorithms (rather than just listing them) and elementary type theory. The main criterion is correctness; other issues are covered in Complexity.

The Signals and Systems course is another crucial link between continuous and discrete modeling. The book by Lee and Varaiya [16] is one of the rare text-books so far that, in addition to providing a good overview of the field, identify and correct most of the numerous notational defects in classical mathematical notations. Such defects have always hampered clean formal reasoning.

Traditional CS topics like Computer Architecture, Operating Systems and Information and Database Systems may have become less central to curriculum design in the past decades, but they are included as yet another opportunity for exercising and consolidating mathematical modeling techniques. This assumes the traditional content is revamped in this spirit.

Needless to say, Programming Languages is not meant to introduce lan-guages, but to provide an introduction to language modeling, e.g., lattices and fixpoints, denotational semantics and more advanced type theory: language the-ory is the materials science for software. Application examples are the languages already encountered via the assignments in other courses (say, Scheme, Haskell, Maple, TLA+, Matlab, Simulink, LabVIEW, VHDL, Java, C++,. . .).

The sequence starting from Physics A to Elements of Quantum Computing expands the students’ horizon with nonstandard computational models.

Software Engineering is left most open to interpretation; the only assump-tion being that it meets the standards of the remainder of the curriculum. The Formal Methods community has generated a wealth of suitable material. Lec-turers may opt for staying within a single series with a wide scope, such as Bjørner’s Software Engineering trilogy [2], or devote a full course to a specific approach (such as refinements) using diverse sources, or any other combination or variant.

(27)

and Embedded Systems in the Automotive Domain. The Automotive , Train -and Avionics Domain are typical examples of domains where a great variety of modeling techniques must be used in harmony. Hence, although such titles may sound specialistic, the content can be given a wide scope. The educational value of topics with this characteristic is well-known in classical engineering, but the domains idea has been given a new impetus for (E)CE by Dines Bjørner [3].

Course metrics The numbers in table 2 indicate course size in units, assuming a 60 units per year system. The design is adaptable to various local situations.

For instance, regulations at our own School of Engineering stipulate per semester 30 units involving 900 hours of study (classes, guided or lab exercises, self-study), amounting to 30 hours per unit. The smallest useful size of a course is 3 units, with classes over 12 weeks at 114h/week. The exam period is 4 weeks. Arithmetic shows that this does not favor activity during the 12 weeks of classes (and that the 900 hours are administrative fiction).

A better option is spreading the courses over 15 weeks, assuming per 3 units weekly 1 hour of classes plus 312 hours of self-study and lab exercises, if any. Own experience at various universities indicates that homework is considerably more effective than guided exercises in stimulating activity1, but puts heavier demands on the staff. Anyhow, the total load of 45 hours/week is reasonable, and low in comparison to what is expected at world-class universities.

3.3 Local and international context

Effects of the local context Thus far, too many universities have been unable to integrate mathematical modeling throughout the CS/CE curriculum or ap-proached the university level considered normal in classical engineering fields.

Still, a well-documented design of an actual curriculum integrating mathe-matics education with software engineering is the BESEME (BEtter Software Engineering through Mathematics Education) project [18].

This report also outlines the impediments to be expected [18, p. 6]:

– Students find it demanding. – Most instructors must revise notes.

In reality, “revising notes” is a euphemism for acquiring essential background [12]. Whereas students are young and (hence supposedly) flexible, many lecturers do not embrace lifelong learning, especially if it entails novel ways of thinking [9]. Here are two more small “case studies” illustrating other concrete situations.

1

(28)

(i) At our School of Engineering, the effects just mentioned have proved quite manifest. As a result, weaving mathematical modeling in the CE curricu-lum remains a faraway target supported by a minority, but felt as a threat by others.

At one stage, our CE program included a course designed like Application-Oriented Formal Logic and a sequel on formal modeling, both non-optional.

The positive effects were most apparent in how students who had taken these courses applied the acquired abilities in their MSc and PhD dissertations under various supervisors who were themselves not even involved in FM.

Still, courses with a strong mathematical content taught by various lecturers, not only in FM but also in classical engineering, got negative evaluations from a few CE students. This was used as an argument by a certain faction among the faculty to clamp down on the classical engineering course involved, and to relegate FM to just one course, for a few last-year students. The fact that foundations are most efective when laid early in the program was well-known.

(ii) In the design of their CS program, our School of Science made a more constructive use of this fact, and placed Application-Oriented Formal Logic with the contents described earlier in the first semester. The professor teach-ing the course is one of the author’s best former students, although scarcity of qualified teaching assistants may have eroded the application-oriented elements somewhat.

These experiences confirm the observation by many authors regarding the overwhelming importance of general acceptance by the faculty, or at least toler-ance from those not wanting to invest effort in new ways of thinking [12, 15, 29]. Other major obstacles against teaching CS/CE at the university level are in-breeding and the idea that CS-related courses can be entrusted to lecturers from a different engineering area (e.g., EE) with just some programming experience. In principle, students pose fewer problems. Of course, in curricula where formal methods courses are isolated, their mathematical content and lack of ap-plications in other courses demotivates some students. This is why, judging from the literature on teaching FM, so much effort is spent on student motivation, and positive results are strongly highlighted (although difficult to measure).

However, consider for the sake of comparison the student acceptance of Mathematical Analysis by the less mathematically inclined students (the math enthusiasts are not at issue here). Much of the acceptance stems from this topic being an unavoidable part of any first and second year engineering program. Choosing engineering means choosing Mathematical Analysis, even for CE ma-jors. Ubiquitous use in other courses confirms relevance in the classical areas.

(29)

accept it more easily as characteristic for university-level (E)CE education. The basis given can then be assumed without further ado in all other courses, pro-viding further consolidation by various applications, which motivates students by confirming relevance. Whether other courses pick up the thread depends on the lecturers, but at least the basis is there and the other courses can evolve gradually. Moreover, with this background the better students will be more de-manding with respect to methodology, and subconsciously or consciously exert gentle pressure on the lecturers if necessary. The attitude of faculty towards this prospect is a decisive factor (and a quality measure), which closes the circle.

In this context, course evaluations must be used wisely. The comments of the students always provide very valuable information for the instructors. However, if students are given the impression (or confirmation) that their feedback is used uncritically for making ad hoc curriculum reforms, their answers will become heavily biased and only serve hidden agendas incompatible with quality.

International context Traditions regarding the mathematical content of engi-neering curricula vary greatly between countries, and are subject to oscillations and mutual feedback.

For instance, Belgian engineering schools used to have very strong mathe-matical requirements, enforced by an entrance examination. The high standards were set since the early 19th century by the Grandes Ecoles and in particular the Ecole Polytechnique in France.

Recent politically-inspired European reforms such as the Sorbonne-Bologna declaration have reshuffled the landscape, increasing the differences they pre-tended to reduce.

For instance, the entrance examination has been cancelled in Flanders, not in Wallonia. The impact has been downplayed, since at that time Flanders scored first among Western countries in the TIMSS (Trends in International Mathemat-ics and Science Study) surveys. However, as a result the mathematically strong programs in secondary school experienced less interest, and declined. As the effects became noticeable in the TIMSS scores, attention shifted to the PISA (Programme for International Student Assessment) criteria. These critera are based on RME (Realistic Mathematics Education), which has strongly influ-enced math education for young children in some Western European countries. As expected, these countries now tend to get a better place in the PISA rankings than they formerly did under TIMSS, creating the illusion of improvement.

(30)

abstraction. These abilities are precisely the most important ones for engineer-ing, classical as well as computer-oriented.

The mathphobia deplored in [28] is certainly not limited to the U.S., where even ample effort is devoted to countering it, but has become a matter of fashion among certain groups of children and adults in Western Europe, even in coun-tries that used to have a strong mathematical tradition. There are indications, needing further study, that some Eastern European countries have escaped this fashion.

Due to these various factors, the mathematical level of students entering en-gineering schools has decreased in various European countries. Since technol-ogy does not comply by lowering its complexity, the first year of the curriculum is important for helping the students to bridge the gap. A framework unifying the mathematics for classical and for computer engineering can be instrumental. The top scores in the TIMSS are achieved by Asian countries. This indicates considerable potential for maintaining universities at a suitable level to meet the challenges of the future. The names in the literature constitute ample evidence. Judging by the faculty lists of universities in various regions, the U.S. appear to have tapped these intellectual resources more effectively than Europe.

The emphasis on mathematics that was consciously maintained throughout this discussion may appear excessive if one sees mathematics just as a collection of tricks and facts, which is the view held by many laypersons. However, the main educational value of mathematics resides in the development of effective problem solving, reasoning and abstraction abilities and the attitudes it imparts.

4 Conclusion

Referring to the quotation by Max Planck, we have argued that the most effec-tive way for making Formal Methods an evident part of everyday practice is not convincing the current practitioners but investing in the education of future gen-erations. Formal Methods, in the sense of mathematical modeling, can be the lever to lift the entire computing curriculum to the scientific and professional level that would be considered acceptable in classical university-level engineer-ing. It goes without saying that this strategy is not directly needed, yet can still be inspiring, for universities where (E)CE education is already world class.

(31)

On the other hand, we have seen that the road to an integrated curriculum is fraught with many impediments, the most important obstacle perhaps being lack of intellectual flexibility and curiosity and, as Gries notes [12], sometimes even mathphobia on the part of the lecturers for the computing-related courses.

The last part of the paper addressed some local and international factors affecting the availability and effective use of intellectual resources in various parts of the world.

One final observation: throughout our argumentations, we have hesitated to invoke one of the primary tasks of a university, because the focus on direct utility in recent years has made even its mentioning suspect. This task is conveying to our students a rich intellectual heritage and stimulating curiosity, and ultimately contributing to their cultural development, not just their professionalism.

Such goals may appear overly ambitious and perhaps lofty today, but the least one can do is avoiding a curriculum ridden with shortcuts.

AcknowledgementThe author thanks the anonymous reviewers for their many helpful comments and observations, some of which appear in the text this paper.

References

1. Harold Abelson and Gerald Jay Sussman with Julie Sussman, Structure and Interpretation of Computer Programs. The MIT Press (1996).

2. Dines Bjørner, Software Engineering (3 volumes). Springer (2006).

3. Dines Bjørner, “What do I mean by Domain?”.http://www2.imm.dtu.dk/˜db/

4. Raymond Boute, “Concrete Generic Functionals: Principles, Design and Applications”, in: Jeremy Gibbons, Johan Jeuring, eds., Generic Programming, pp. 89–119, Kluwer (2003). 5. Raymond Boute, “Can lightweight formal methods carry the weight?”, in: David Duce

et al., eds., Teaching Formal Methods 2003, Oxford Brookes University (2003). Web:

http://cms.brookes.ac.uk/tfm2003/papers/boute.pdf

6. Raymond Boute, “Functional declarative language design and predicate calculus: a practical approach”, ACM Trans. Prog. Lang. Syst. 27, 5, pp. 988–1047 (2005).

7. Raymond Boute, “Calculational semantics: deriving programming theories from equations by functional predicate calculus”, ACM Trans. Prog. Lang. Syst. 28, 4, pp. 747–793 (Jul. 2006).

8. James B. Dabney and Thomas L. Harman, Mastering Simulink 4 (2nd ed.). Prentice Hall (2001).

9. Edsger W. Dijkstra, “How Computing Science created a new mathematical style”, EWD 1073. University of Texas at Austin (Mar. 1990).

Web:http://www.cs.utexas.edu/users/EWD/ewd10xx/EWD1073.PDF

10. Ganesh Gopalakrishnan, Computation Engineering: Formal Specification and Verification Methods (Aug. 2003).

Web:http://www.cs.utah.edu/classes/cs6110/lectures/CH1/ch1.pdf

11. David Gries and Fred Schneider, A Logical Approach to Discrete Math. Springer (1993). 12. David Gries, “The need for education in useful formal logic”, IEEE Computer 29, 4, pp.

(32)

13. Henri Habrias and S´ebastien Faucou, “Linking Paradigms, Semi-formal and Formal Nota-tions”, in: C. Neville Dean and Raymond T. Boute, eds., Teaching Formal Methods, pp. 166–184, Springer LNCS 3294 (Nov. 2004).

14. Leslie Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Soft-ware Engineers. Addison-Wesley (2002).

Web:http://research.microsoft.com/users/lamport/tla/book.html

15. Edward A. Lee and Pravin Varaiya, “Introducing Signals and Systems — the Berkeley Approach”. First Signal Processing Education Workshop, (Oct. 2000).

Web:http://ptolemy.eecs.berkeley.edu/publications/papers/00/spe1/

16. Edward A. Lee and Pravin Varaiya, Structure and Interpretation of Signals and Systems. Addison-Wesley (2003).

17. Timothy C. Lethbridge, “What knowledge is important to a software professional?”, IEEE Computer 33 5, pp. 44–50 (May 2000).

18. Rex L. Page, “Software is discrete mathematics”.

Web:http//www.cs.ou.edu/˜beseme/besemePres.pdf

19. A. Parkin, “Professional Programmers – Do They Read?”, Computer Bulletin, Series II, 4, p. 23 (1975).

20. David L. Parnas, “Education for computing professionals”, IEEE Computer 23, 1, pp. 17–22 (Jan. 1990).

21. David L. Parnas, “Predicate Logic for Software Engineering”, IEEE Trans. SWE 19, 9, pp. 856–862 (Sep. 1993).

22. Anthony Ralston, “Let’s Abolish Pencil-and-Paper Arithmetic”. Journal of Computers in Mathematics and Science Teaching, Vol. 18, No. 2, pp. 173–194 (1999).

Web:http://www.doc.ic.ac.uk/˜ar9/abolpub.htm

23. John Rushby and Natarajan Shankar, “Theorem Proving and Model Checking for Software”, Tutorial, Fourth Symposium on the Foundations of Software Engineering (Oct. 1996). Web:http://www.csl.sri.com/users/rushby/slides/fse4tut.ps.gz

24. Joel Spolsky, “The Perils of Java Schools”, in: Joel on Software (Dec. 2005).

Web:http://www.joelonsoftware.com/articles/ThePerilsofJavaSchools.html

25. Joel Spolsky, “Stackoverflow.com”, in: Joel on Software (Apr. 2008).

Web:http://www.joelonsoftware.com/items/2008/04/16.html

26. Gerald Jay Sussman and Jack Wisdom with Meinhard E. Mayer, Structure and Interpretation of Classical Mechanics. The MIT Press (2001).

27. George B. Thomas, Maurice D. Weir, Joel Hass, Frank R. Giordano, Thomas’s Calculus, 11th ed. Addison Wesley (2004).

28. Allen B. Tucker, Charles F. Kelemen, Kim B. Bruce, “Our Curriculum Has Become Math-Phobic!”, ACM SIGCSEB, SIGCSE Bulletin 33 (2001).

Web:http://citeseer.ist.psu.edu/tucker01our.html

29. Jeannette M. Wing, “Weaving Formal Methods into the Undergraduate Curriculum”, Proc. 8th Intl. Conf. on Algebraic Methodology and Software Technology (AMAST) pp. 2–7 (May 2000). Web:

(33)

An Introductory Course on Programming based on

Formal Specification and Program Calculation

Nazareno Aguirre1, Javier Blanco2, Mar´ıa Marta Novaira1, Sonia Permigiani1, Gast´on Scilingo1

1 _{Departamento de Computaci´on, FCEFQyN, Universidad Nacional de R´ıo Cuarto, Argentina,}

{naguirre,mnovaira,spermigiani,gaston}@dc.exa.unrc.edu.ar

2 _{Facultad de Matem´atica, Astronom´ıa y F´ısica, Universidad Nacional de C´ordoba, Argentina,}

[email protected]

Abstract. In this paper, we report on our experience in teaching introductory courses on programming based on formal specification and program calculation, in two different Computer Science programmes. We favour the use of logic as a tool for software development, the notion of program as a formal entity, as well as some issues associated with efficiency. We also review and use in practical cases some important program transformation strategies, such as generalisation, tupling and modularisation.

We will describe our approach, as well as the advantages and drawbacks that we have observed over the years teaching these courses.

1 Introduction

(34)

Some approaches related to the use of formal methods in introductory courses to programming have an emphasis on program verification. Often, these courses are based on structured programming, and tend to treat program verification as a task to be performed after one constructs a program. In our opinion, based on our own experience, and discussions with students and colleagues, this generally leaves students the feeling that verification is an additional “burden”. Further-more, if this is combined with the fact that usually one picks relatively simple problems for teaching programming and verification in introductory courses, students are typically left with the feeling that verification is not only additional burden, but also optional burden (students get the idea that they have to verify programs that they already know to be correct).

(35)

2 Description of the Course

As explained before, the course we are describing here is an introductory course on programming taught at two different Universities. In the National Univer-sity of C´ordoba, the course is taught during the first two semesters of a 5-year Computer Science programme. In the National University of R´ıo Cuarto, on the other hand, the course is taught during the third and fourth semesters, again of a 5-year Computer Science programme. In the former, students have no previous courses on programming or logic, but they take simultaneously with this course one on discrete mathematics; In the latter case, when students start the course they had already taken a 2-semester introduction to imperative programming course, and a basic course on mathematical logic.

Although the course is taught in different contexts in the two Universities, we seek achieving the same general goals. Essentially, we want the students to accomplish the following:

– Develop the ability to formalise problems, using logic as a tool.

– View specifications and programs as formal entities, and consider program-ming as the manipulation of these formal entities.

– Obtain considerable training on using recursion as a powerful mechanism for defining functions/programs.

– Understand that reasoning about functions can be exploited not only in func-tional programming, but also in imperative programming (particularly via transformation schemata).

– Get acquainted with a very elementary theory of abstract data types (and its relevance in program development).

The contents of the course is composed of the following three main modules:

– Logic and specifications. We employ an equational version of predicate logic with generalised quantifiers [7] (see also [9, 6]). The main goal is to have a suitable tool for reasoning with large formulae (mainly programs). This logic is used for both the functional and the imperative paradigm. – Construction of functional programs. The students learn how to formally

(36)

– Construction of imperative programs. This module is rather traditional (see for example [5, 8, 6, 11, 4]). We try, however, to use what was learned in the previous module to help in this process. The main tool is to translate functional programs into the imperative formalism by using tail recursion, which not only allows us to translate the program itself, but also its proof of correctness. Although the underlying computational models are different in the functional and imperative paradigms, the students can get the feeling that proofs in the two contexts share similar ideas (e.g., invariants can be seen as a restricted way to use induction). Also when introducing impera-tive programming, students are faced with the notion of abstract data type. We employ the case of lists (which are somehow inherent to functional gramming) and an array based implementation of lists in imperative pro-gramming, to show how functional programs handling lists are transformed into imperative programs manipulating arrays. The usual formal concepts of abstraction function, representation invariant and the like are used superfi-cially.

3 A Sample Exercise

In order to better illustrate our approach, and the notation used, let us provide an example, which is an exercise used in the course. Consider the problem of, given a listxsof integers, finding the sum of the elements in the segment of minimum sum ofxs. A segment ofxsis simply any sublist ofxs. So, for instance, if list xs is [1,-4,-2,1,-5,8,-7], then the minimum sum segment of xs is [-4,-2,1,-5], and its sum equals-10; if we consider the list[1,2], then its minimum sum segment is[]. This problem has been discussed by various researchers (particularly in the context of program transformation), for example in [2, 3, 10].

A first step is to formally specify the problem. For this task, the specification language we use provides generalised quantified expressions (with general rules for dealing with these), which can be built out of any binary operator, as long as it admits a neutral element, and is associative and commutative. This style is similar to that used in [9] The generalised expression corresponds to applying the operator under consideration to a range of values. The operator Min satis-fies the above conditions, and therefore can be used in a quantified expression, allowing us to straightforwardly specify the problem in the following way:

minSum.xs=hMinas, bs, cs:xs=as++bs++cs:sum.bsi

(37)

from the above specification is done via induction on the length of xs. A de-tailed calculation of functionminSumcan be found in [10], page 147. The re-sulting recursive function is the following:

minSum.[] = 0

minSum.(x ⊲ xs) =g.(x ⊲ xs)minminSum.xs

wheregis defined as follows:

g.[] = 0

g.(x ⊲ xs) = 0min(x+g.xs)

From these functions, we can do various things. For instance, we can em-ploy schemata for transforming the above functions to tail recursive versions, and from the resulting functions straightforwardly obtain imperative programs. Also, we could attempt to derive a more efficient version of minSum, using transformation strategies (in this case, tupling is a suitable one). The resulting more efficient version ofminSum, obtainable using tupling onminSumandg, is the following:

h.[] = (0,0)

h.(x ⊲ xs) = ((x+b)mina,0min(x+b))

|[(a, b) =h.xs]|

4 Experiences in the two Programmes

We have been using the described approach for the past 10 years in the National University of C´ordoba, and for the past 6 years in the National University of R´ıo Cuarto. The experience we gained along these years enabled us to improve the course in various respects, in particular, collect better exercises, with interesting non trivial solutions, illustrating some of the benefits of program calculation. This task has benefited from newer mature bibliography, such as [1], and in-cluding bibliography in Spanish (e.g., [12, 13]).

(38)

(e.g., provide pre- and post- conditions for methods in object oriented imple-mentations of abstract data types), write well structured programs, and exploit recursion when solving problems in imperative and object oriented languages. In general, good students tend to appreciate formal methods and their associated benefits, which is evidenced in the optional courses they choose later on in the programmes, and the topics they choose for their final projects. We also detected a number of drawbacks. First, about 50% of the students fail the course. This seems to be a very critical point against the approach; however, previous ver-sions of the introductory courses (more traditional ones) had roughly the same failure rate. This is the case in both Universities. In the case of the University of C´ordoba, where the course is taught in the first year of the Computer Science programme, a great part of the students failing the course switch to a different programme (this is normal in the first year of most programmes in Argentina). In the case of the University of R´ıo Cuarto, on the other hand, the 50% failure rate in the second year of a programme is not normal (although it has been the usual for this course, even for previous, more traditional, versions of it). In both Universities, students failing the course can take it again the following year (i.e., they are not forced to abandon the corresponding programmes).

Another important drawback is that the average student usually becomes too “syntactic” (or “mechanical”) in reasoning about programs, which has a negative impact in abstraction. In particular, it is usually rather difficult for stu-dents to “jump” in and out from the calculus (i.e., take perspective on the situ-ation of the derivsitu-ation at hand, and decide accordingly). In order to overcome this problem, we are currently seeking for an integration between the described course and a later course on data abstraction and the implementation of abstract datatypes. We hope that as a result of this integration the students will have a chance to exercise the role of abstraction in problem solving, which requires them to combine thinking outside the calculus, for designing data representa-tions, and using the calculus, for deriving correct implementations for the oper-ations associated with the data abstractions.

5 Conclusions

(39)

in C´ordoba. We believe this might be due to the case that, since the students have already learned the basics of programming in an informal setting, most tend to feel that the rigour associated with the program calculus used in the course is not necessary for programming. Solving more complicated problems, compared to those in their first course, and developing more sophisticated solutions, helps in making students appreciate the benefits of a calculational approach. Students in R´ıo Cuarto also exhibit a greater resistance, compared to students in C ´ordoba, to learning and applying logic for specification.

As work in progress, we are starting to conduct a more thorough study of the consequences of our approach, mostly based on qualitative analysis.

References

1. R. Backhouse, Program Construction, Calculating Implementations from Specifications, Wi-ley, 2003.

2. J. Bentley, Programming Pearls, second edition, Addison-Wesley, 2000.

3. R. Bird, Algebraic Identities for Program Calculation, The Computer Journal, 32(2), Oxford University Press, 1989.

4. E. Cohen, Programming in the 1990s: An Introduction to the Calculation of Programs, Springer-Verlag, 1990

5. E. Dijkstra, A Discipline of Programming, Prentice Hall, 1976.

6. E. Dijkstra and W. Feijen, A Method of Programming, Addison-Wesley, 1988.

7. E. Dijkstra and C. Scholten, Predicate Calculus and Program Semantics, Monographs in Computer Science, Springer-Verlag, 1990.

8. D. Gries, The Science of Programming, Monographs in Computer Science, Springer-Verlag, 1981.

9. D. Gries and F. Schneider, A Logical Approach to Discrete Math, Monographs in Computer Science, Springer-Verlag, 1993.

10. R. Hoogerwoord, The Design of Functional Programs: A Calculational Approach, PhD The-sis, Eindhoven University of Technology, The Netherlands, 1989.

11. A. Kaldewaij, Programming: The Derivation of Algorithms, Prentice Hall, 1990.

12. N. Mart´ı-Oliet, Y. Ortega-Mallén and J. Verdejo-López, Estructuras de Datos y Métodos Algor´ıtmicos, Ejercicios Resueltos, Pearson Educación, 2004.